Nuprl Definition : int_iseg
13,42
postcript
pdf
{
i
...
j
} == {
k
:
| (
i
k
) & (
k
j
)}
latex
Up
int
1
,
int
1
Wellformedness Lemmas
int
iseg
wf
,
int
iseg
wf
Definitions
{
x
:
A
|
B
(
x
)}
,
,
P
&
Q
,
A
B
FDL editor aliases
int_iseg
origin
| (i 
k) & (k j)} | (i k) & (k j)} B